Nuprl Lemma : bnot_thru_band
9,38
postcript
pdf
p
,
q
:
. (
(
p
q
)) = ((
p
)
(
q
))
latex
ProofTree
Definitions
t
T
Lemmas
bool
wf
,
btrue
wf
,
bfalse
wf
origin
p,q:
. (
(p 
q)) = ((p) 
(q)) 
p,q:. ((p q)) = ((p) (q))
T